Nuprl Definition : rationals
11,40
postcript
pdf
rationals == quotient(b-union(
; (
:
int_nzero));
r
,
s
.(qeq(
r
;
s
) = tt))
latex
clarification:
rationals == quotient(b-union(
; (
:
int_nzero));
r
,
s
.(qeq(
r
;
s
) = tt
))
latex
Definitions
tt
,
qeq(
r
;
s
)
,
,
s
=
t
,
int_nzero
,
,
x
:
A
B
(
x
)
,
b-union(
A
;
B
)
,
quotient(
A
;
x
,
y
.
B
(
x
;
y
))
FDL editor aliases
rationals
origin